V:(IdType), M1, M2:MsgA.
(x:Id. V(x) r M2.ds(x))  M1  M2  (x:Id, v:(V(x)). M2.init(x,v)  M1.init(x,v)) 

latex

Definitions	M.init(x,v), M1  M2, M.ds(x), MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), <a, b>, x  dom(f), , s = t, suptype(S; T), x(s), f(x), Top, a:A fp B(a), , x. t(x), x.A(x), IdDeq, S  T, f(x)?z, Void, Type, f(a), IdLnk, Knd, Id, f  g, t  T, x:A. B(x), b, A c B, x:A  B(x), P  Q, x:AB(x), left + right, Unit, P  Q, , b, A, #$n, , False
Lemmas	subtype rel self, int inc rationals, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, Id wf, id-deq wf, fpf-cap wf, rationals wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-dom wf, assert wf, ma-init wf, ma-sub wf, ma-ds wf, msga wf